1. Field of the Invention
The present invention relates generally to logic verification techniques at the stage of designing logic circuits, and more particularly to a logic verification technique intended for logic circuits described in a CPU-executable programming language.
2. Description of the Related Art
LSI design automation/support techniques, developed to automate or support design tasks, are generally employed for designing LSIS or VLSIs. One typical process of VLSI designing processes which employ the LSI design automation/support technology is a top-down design process using various EDA (electronic design automation) tools. Top-down design of this type can be generally divided into system design, functional design, logic design and layout design from upstream to downstream steps. A description of the top-down design will be given below with reference to FIG. 1.
Preparation of system specification begins with description of LSI behaviors by treating the whole LSI as a system. The description is called a behavioral level description 12. The behavioral level description 12 is prepared, for example, in a natural language, HDL (hardware description language) such as VHDL or Verilog HDL or programming language such as C, C++ or Java. The behavioral level description 12 may also be prepared in other programming language such as SystemC or SpecC which incorporates additional features convenient for representing circuits in C or C++.
The behavioral level description 12 is next converted into an RT level (register transfer level) description 14 in behavioral synthesis phase. The RT level description 14 is normally written in HDL or a programming language. Heretofore, it has often been customary to manually perform the behavioral synthesis phase to generate an RTL description using an HDL (hardware description language).
Then, the RT level description 14 is automatically converted into a gate level description (gate level logic circuit: net list) 1D in logic synthesis phase. Layout design is conducted based on the net list thus generated followed by chip design.
Design verification, aimed at validating the design performed in the steps, is also important in LSI design. Design verification is comprised, for example, of equivalence verification which verifies whether the conversion in each synthesis phase is correct and specification verification which verifies whether each description correctly represents the LSI to be designed.
Simulation or formal verification has conventionally been employed for equivalence verification.
Equivalence verification by simulation performs simulation by giving the same test patterns to two descriptions to be compared and examines whether the result equivalent to the desired one. Simulation is performed using a dedicated simulator when the descriptions are represented in HDL as with the RT level description 14. On the other hand, when the descriptions are represented in a programming language as with the behavioral level description 12, simulation is performed by converting the descriptions into a CPU-executable format (called object codes) with a compiler and then directly executing the obtained object codes 15 with the CPU.
Formal equivalence verification uses a mathematical method to verify whether two combinational circuit logics are equivalent. FIG. 2 illustrates a block diagram showing the common configuration of a formal equivalence verification apparatus designed to verify equivalence between the RT level description 14 and the gate level description 1D.
Referring to FIG. 2, the RT level description is represented by reference numeral 14 and the gate level description by reference symbol 1D. Correspondence information is indicated by reference numeral 13 which describes a correspondence relation between signals to be compared at two levels. The signals to be compared are primary inputs, primary outputs, registers and other internal terminals specified by the designer. The signals are referred as the comparison signals. Logic cone extraction sections are represented by reference numeral 23, which extract logic cones respectively from the RT level description and the gate level description. A logic cone refers to a combinational circuit required to determine signal logic, which is represented by a Boolean expression. Extraction of logic cones is made by using a method such as that shown in Document 1: Malik, S. et al, “Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment”, Proceedings of IEEE International Conference on Computer-Aided Design, pp. 6-9, 1988 More specifically, a logic cone can be obtained by tracing the combinational circuit from a comparison signals to its input. Extracted logic cones are indicated respectively by reference symbols 18 and 1E. Logic cone comparison section are represented by reference numeral 24, which examine logical equivalence of Boolean expressions of the logic cones each corresponding comparison signals. The logic cone extraction section 24 determines that the RT level description 14 and the gate level description 1D are logically equivalent when the logic cones of all the corresponding comparison signals are logically equal, and produces the comparison result to the output device 3.
A formal equivalence verification apparatus for verifying equivalence between the RT level description 14 and the gate level description 1D, similar to FIG. 2, is also disclosed in Japanese Patent Application Unexamined Publication No. 8-22485.
Specification verification is also provided with a known technique, namely, property verification by using simulation or formal method, as with equivalence verification. Specification verification by simulation examines whether the circuit has the desired functionality by giving test patterns to the descriptions to be compared during simulation and analyzing the simulation result. Property verification by formal method statically and mathematically checks whether a given description meets desired properties. Formal property verification is referenced in Document 2: Edmund M. Clarke, et al. “Model Checking”, pp 61-74, The MIT Press, 1999. FIG. 3 illustrates a block diagram of configuration of a formal property verification apparatus designed to verify whether the ordinary RT level description 14 meets given properties.
Referring to FIG. 3, the RT level description is represented by reference numeral 14 while the properties to be met by the circuit are indicated by reference symbol 1C. The properties 1C include “no deadlock by the circuit” and “response returned within fixed cycles upon receipt of request signal”. The logic cone extraction section 23 extracts logic cones 18 from the RT level description 14. Model checking section 25 enumerates a set of possible signal value combinations (called states). When the set of all possible states of the circuit is enumerated, the model checking section 25 checks whether the set meets the given properties.
Property verification by formal method does not need test data unlike simulation and is capable of completely verifying whether the given properties are met.
With growing scale of integration in resent years, LSIs to be comprised of several millions of gates, and faster verification is becoming critical in specification verification which verifies whether designed circuits have the intended functionality.
The common technique for specification verification is by simulation; however, simulation of the RT level description 14 is becoming more time-consuming as a result of larger scale of integration in circuits available today. In contrast, specification verification at behavioral level tends to be very abstract and fast. Additionally, simulation can be performed using a rich collection of libraries available in the programming language used. For this reason, it is common to represent the behavioral level description 12 in a programming language and convert it into the CPU-executable object code 15 by a compiler and directly execute the object code 15 by the CPU for fast simulation, as shown in FIG. 1. Further, the behavioral level description 12 represented in a programming language is automatically converted into the RT level description 14 by behavioral synthesis phase.
Tools used for such synthesis are in fact commonly comprised of software. However, such tools are not necessarily bug-tree, and therefore verification is needed in each synthesis phase to verify whether synthesis has been properly performed.
The conventionally most popular verification in behavioral synthesis phase is simulation using test patterns; however, this simulation presented the following problems:
Simulation using test patterns naturally requires generation of test patterns, thus requiring time and costs for such a task. Moreover, the nature of synthesis which can be verified by simulation depends on test patterns, thus making it impossible to verify errors not considered in the test patterns. Consequently, there was a possibility that the conventional equivalence verification by simulation could not yield a satisfactory result. Further, repetition of simulation at two levels, namely, behavioral level and RT level, runs counter to the object of introducing behavioral synthesis which is to ensure faster verification.
Other techniques under study for verification of the RT level description 14 against the behavioral level description 12 include formal verification of equivalence between the RT level description 14 and the behavioral level description 12.
An example of behavioral synthesis verification apparatus is described in Document 3: “Formal Methods in System Design, No. 16, pp. 59-91, 2000.”
The behavioral synthesis verification apparatus described in the Document 3 outputs 1) formal specification description, 2) correctness lemmas and 3) verification scripts for a theorem proving system called PVS, from a behavioral description, the RT level description and the correspondence relation which is a by product of behavioral synthesis. A correctness lemma refers to a logic formula representing such conditions that, changes in values of pairs of comparison signals are the equivalent for all execution paths (state series) of behavioral description and RT level description respectively. In the Document 3, the execution paths are limited to those which does not include branching/confluence structure. The correspondence relation mentions which pair of comparison signals are corresponding between the behavioral description and the RT level descriptions. The correspondence relation also mentions which pair of execution paths are corresponding between the two descriptions. According to generated verification scripts, the PVS uses a symbolic term rewriting method along with the execution paths to generate functions, each of which represents a change in comparison signal along with the given execution path. Then, the PVS examines whether the functions representing changes in signal values are equivalent for each pair of corresponding comparison signals and for each pair of corresponding execution paths. The PVS verifies equivalence between the behavioral description and the RT level description by showing that the generated functions are equivalent for all pairs of corresponding comparison signals and for all pairs of corresponding execution paths.
Another example of behavioral synthesis verification apparatus is described in Document 4: “International Conference on Computer Design, pp. 456-466, 1999.”
The behavioral synthesis verification apparatus in the Document 4 is basically identical to the apparatus described in the Document 3. The apparatus described in the Document 4 does not restrict the execution paths to be basic block. The loops of the repetition structure (loops structure) of original behavioral description are unrolled until correspondence relations between the execution paths of the behavioral description and the ones of RT level description are found. The technique called symbolic simulation is employed rather than symbolic term rewriting to generate functions representing changes in signal values.
The prior art as described above has exclusively used the above method to verify equivalence between the behavioral level description 12 and the RT level description 14, and not much emphasis has been placed on verification of equivalence between the object code 15 compiled from the behavioral level description 12 and the RT level description 14.
For this reason, there has been a possibility that equivalence cannot be guaranteed between a result of execution of the object code 15 compiled from the behavioral level description 12 by the CPU and the execution result of operations of the actual circuit designed from the behavioral level description 12. Since meanings of languages can be changed by libraries linked during compiling in many programming languages, there is not necessarily a guarantee that the behavioral level description 12 and the object code 15 compiled from the behavioral level description 12 are equivalent. Additionally, since compilers, designed to convert the behavioral level description 12 into a CPU-executable format, are comprised of software, they are not necessarily free of bugs, occasionally causing the behavioral level description 12 to be unequivalent to the object code 15. If the behavioral level description 12 and the object code 15 are not equivalent, the RT level description 14, derived from the behavioral level description 12, is not equivalent to the object code 5, thus making it impossible to determine that the operations of the RT level description 14 are correct even if the operations of the object code 15 are found to be correct as a result of execution of this code. This can result in the designer erroneously proceeding with the next phase, namely, logic synthesis phase despite the fact that operational check has not been correctly performed in behavioral synthesis phase.
This is the reason why a logic verification system is desired which can guarantee equivalence between an execution result of the object code 15 compiled from the behavioral level description 12 and an execution result of operations of the circuit obtained from behavioral synthesis.
There are also demands for formal property verification on the behavioral level description 12. In this case, since formal property verification and simulation are complimentary to each other, it is preferable that operations executed by the CPU, that is, the object code 15 can be verified.
To implement these logic verification capabilities using logic cones, a technique is required which can extract logic cones from the CPU-executable object code since conventional logic cone extraction techniques, designed to extract logic cones from HDL or gate level descriptions, cannot be used.